Definitions | IdLnk, t T, Id, f(a), Type, x,y. t(x;y), x:A. B(x), x. t(x), kindcase(k; a.f(a); l,t.g(l;t) ), AtomFree(T;x), Knd, x:AB(x), x:AB(x), <a,b>, b, ESAtomAxiom{i:l}(T;V), isrcv(k), True, T, P Q, SqStable(P), {x:A| B(x) }, Void, x:A. B(x), Top, S T, x.A(x), ESAxioms(E;T;M;loc;kind;val;when;after;sends;sender;index;first;pred;causl), Prop, A, , lnk(k), Msg_sub(l;M), ||as||, #$n, {i..j}, type List, eventtype(k;loc;V;M;e), EqDecider(T), Unit, , mk-es0(E;eq;T;V;M;loc;k;v;w;a;snds;sndr;i;f;prd;cl;p;q), ES0, P & Q |